
(* ========================================================================== *)
(*  The Robbins Conjecture                                                    *)
(* ========================================================================== *)

(* 
   Given a unary (' or []) and an associative, commutative binary
   operator (juxtoposition) satisfying the axiom [[ab][ab']] = a,
   show that there exists c, d such that
   [cd] = c'.

   The proof follows Hales paper Formal Proof, p. 1378 of the Notices
   of the AMS, Vol 55 #11.  The proof sketch given there is as
   follows.  Fix the following variables:
   
   x
   u = [xx']  
   c = x^3u
   d = xu
   j = [cd]
   e = u[x^2]c'

   = with no sign indicates an expanding of variables.  = with a
   number indicates using the given lemma.

   0 : [u[x^2]] = [[xx'][xx]] =' x. 

   1 : [xu[xu[x^2]c']] =' [[[xux^2 ][xu[x^2]]][xu[x^2]c']] 
                       =  [[c'[xu[x^2]]][c'xu[x^2]]] =' c'

   2 : [uc'] =  [u[x^2ux]] 
             =0 [u[x^2u[u[x^2]]]]
             =' [[[ux^2][u[x^2]]][x2 u[u[x^2]]]] 
             =' [u[x^2]] 
             =0 x. 

   3 : [ju] =  [[xcu]u] 
             =' [[xcu][[uc][uc']]] 
             =2 [[xcu][x[cu]]] 
             =' x 

   4 : [x[x[x^2]uc']] =  [[[x[uc']][xuc']][x[x^2]uc']] 
                      =2 [[[x^2][xuc']][[x^2]xuc']] 
                      =' [x^2] 

   5 : [xc'] =1 [x[xu[xu[x^2]c']]] 
             =0 [[u[x^2]][xu[xu[x^2]c']]] 
             =  [[u[x^2]][ux[xe]]] 
             =4 [[u[x[xe]]][ux[xe]]] 
             =' u 

   6 : [jx] =' [j[[xc][xc']]] 
            =5 [j[[xc]u]] 
            =  [[uxc][u[xc]]] 
            =' u 

   7 : [cd] =  j 
            =' [[j[xc']][jxc']] 
            =5 [[ju][jxc']] 
            =3 [x[jxc']] 
            =2 [[c'u][c'jx]] 
            =6 [[c'[jx]][c'jx]] 
            =' c'  

Rewriting in just the right spot is tricky.  We accomplish this usually by using
the handy PATH_CONV.
*) 

(* 
#use "hol.ml";; 
*) 

prioritize_num();;
overload_interface("*",`( fn ):num->num->num`);;
override_interface("neg",`( neg ):num->num`);;

(* -------------------------------------------------------------------------- *)
(*  Util                                                                      *)
(* -------------------------------------------------------------------------- *)

let list x = [x];;

let ABBREV_LABEL_TAC : term -> string -> tactic =
  fun t lab -> 
  ABBREV_TAC t THEN
  FIRST_ASSUM (fun thm -> UNDISCH_TAC (snd (dest_thm thm))) THEN
  DISCH_THEN (LABEL_TAC lab);;

let ABBREV_LABEL_TAC : term -> string -> tactic =
  fun t lab -> 
  ABBREV_TAC t THEN POP_ASSUM MP_TAC  THEN 
  DISCH_THEN (LABEL_TAC lab);;

let SUBGOAL_THEN_MESON : thm list -> term -> thm_tactic -> tactic =
  fun thms t ttac -> SUBGOAL_THEN t ttac THENL [ASM_MESON_TAC thms; ALL_TAC];;

(* -------------------------------------------------------------------------- *)
(*  Proof                                                                     *)
(* -------------------------------------------------------------------------- *)

let robbins = prove(
  `(!x y. x * y = y * x) ==> 
   (!x y z. x * (y * z) = (x * y) * z) ==> 
   (!a b. neg(neg(a * b) * neg(a * neg b)) = a) ==> 
   (?c d. neg(c * d) = neg c)`,
  DISCH_THEN (LABEL_TAC "COM") THEN 
  DISCH_THEN (LABEL_TAC "ASS") THEN 
  DISCH_THEN (LABEL_TAC "ROB") THEN 
  ABBREV_LABEL_TAC `u = neg(x * neg x)` "U" THEN 
  ABBREV_LABEL_TAC `d = x * u` "D" THEN 
  ABBREV_LABEL_TAC `c = x * x * x * u` "C" THEN 
  ABBREV_LABEL_TAC `j = neg(c * d)` "J" THEN 
  ABBREV_LABEL_TAC `e = u * neg(x * x) * neg c` "E" THEN 
  EXISTS_TAC `c:num` THEN 
  EXISTS_TAC `d:num` THEN  
  (* Step 0 *)
  SUBGOAL_THEN `neg(u * neg(x * x)) = x` (LABEL_TAC "H0") THENL
  [EXPAND_TAC "u" THEN 
   USE_THEN "COM" (ONCE_REWRITE_TAC o list) THEN 
   USE_THEN "ROB" (ONCE_REWRITE_TAC o list) THEN 
   REFL_TAC;
  (* Step 1 *)
  SUBGOAL_THEN `neg(x * u * neg(x * u * neg(x * x) * neg c)) = neg c` (LABEL_TAC "H1") THENL 
  [USE_THEN "ROB" (fun thm -> CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV[SYM (SPECL [`neg c:num`;`x * u * neg(x * x)`] thm)]))) THEN 
   USE_THEN "COM" (CONV_TAC o RAND_CONV o ONCE_REWRITE_CONV o list) THEN 
   USE_THEN "C" (CONV_TAC o PATH_CONV "rrl" o ONCE_REWRITE_CONV o list o SYM) THEN 
   SUBGOAL_THEN_MESON[] `x * x * x * u = (x * u) * (x * x)` (REWRITE_TAC o list) THEN
   SUBGOAL_THEN_MESON[] `neg c * x * u * neg (x * x) = x * u * neg(x * x) * neg c` (REWRITE_TAC o list) THEN
   SUBGOAL_THEN_MESON[] `x * u * neg (x * x) = (x * u) * neg(x * x)` (REWRITE_TAC o list) THEN
   USE_THEN "ROB" (ONCE_REWRITE_TAC o list) THEN 
   ASM_MESON_TAC[];
  (* Step 2 *)
  SUBGOAL_THEN `neg(u * neg c) = x` (LABEL_TAC "H2") THENL
  [EXPAND_TAC "c" THEN 
   SUBGOAL_THEN_MESON[] `x * x * x * u = (x * x * u) * x` (REWRITE_TAC o list) THEN
   USE_THEN "H0" (CONV_TAC o PATH_CONV "lrrrrr" o ONCE_REWRITE_CONV o list o SYM) THEN  
   USE_THEN "H0" (CONV_TAC o RAND_CONV o ONCE_REWRITE_CONV o list o SYM) THEN  
   USE_THEN "ROB" (fun thm -> CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV[SYM (SPECL [`neg (u * neg(x * x)):num`;`x * x * u:num`] thm)]))) THEN 
   USE_THEN "ROB" (fun thm -> ONCE_REWRITE_TAC[SPECL [`u:num`;`x * x`] thm]) THEN 
   SUBGOAL_THEN_MESON[] `x * x * u = u * (x * x)` (ONCE_REWRITE_TAC o list) THEN 
   USE_THEN "COM" (CONV_TAC o PATH_CONV "rrrr" o ONCE_REWRITE_CONV o list) THEN 
   USE_THEN "ROB" (ONCE_REWRITE_TAC o list) THEN 
   ASM_MESON_TAC[];
  (* Step 3 *) 
  SUBGOAL_THEN `neg (j * u) = x` (LABEL_TAC "H3") THENL
  [SUBGOAL_THEN_MESON[] `j = neg(x * c * u):num` (REWRITE_TAC o list) THEN  
   USE_THEN "ROB" (CONV_TAC o RAND_CONV o ONCE_REWRITE_CONV o list o SYM o SPECL [`x:num`;`c * u:num`]) THEN 
   USE_THEN "H2" (CONV_TAC o PATH_CONV "rrr" o ONCE_REWRITE_CONV o list o SYM) THEN 
   REPEAT AP_TERM_TAC THEN ASM_MESON_TAC[];
  (* Step 4 *)  
  SUBGOAL_THEN `neg (x * neg (x * neg (x * x) * u * neg c)) = neg(x * x)` (LABEL_TAC "H4") THENL
  [USE_THEN "ROB" (CONV_TAC o RAND_CONV o ONCE_REWRITE_CONV o list o SYM o SPECL [`neg (x * x):num`; `x * u * neg c:num`]) THEN 
   USE_THEN "ROB" (CONV_TAC o PATH_CONV "lrrl" o ONCE_REWRITE_CONV o list o SYM o SPECL [`x:num`; `u * neg c:num`]) THEN 
   USE_THEN "H2" (REWRITE_TAC o list) THEN 
   AP_TERM_TAC THEN 
   USE_THEN "COM" (CONV_TAC o RATOR_CONV o ONCE_REWRITE_CONV o list) THEN 
   BINOP_TAC THEN ASM_MESON_TAC[];
  (* Step 5 *)
  SUBGOAL_THEN `neg(x * neg c) = u:num` (LABEL_TAC "H5") THENL 
  [USE_THEN "ROB" (CONV_TAC o RAND_CONV o ONCE_REWRITE_CONV o list o SYM o SPECL [`u:num`; `x * neg(x * e):num`]) THEN 
   USE_THEN "E" (CONV_TAC o PATH_CONV "rrr" o REWRITE_CONV o list o SYM) THEN 
   SUBGOAL_THEN_MESON[] `x * u * neg(x*x) * neg c = x * neg(x*x) * u * neg c` (ONCE_REWRITE_TAC o list) THEN 
   USE_THEN "H4" (REWRITE_TAC o list) THEN 
   EXPAND_TAC "e" THEN 
   USE_THEN "H0" (REWRITE_TAC o list) THEN 
   SUBGOAL_THEN_MESON[] `!p. u * x * p = x * u * p` (REWRITE_TAC o list) THEN  
   USE_THEN "H1" (REWRITE_TAC o list) THEN 
   ASM_MESON_TAC[];
  (* Step 6 *) 
  SUBGOAL_THEN `neg(j * x) = u` (LABEL_TAC "H6") THENL
  [USE_THEN "ROB" (CONV_TAC o PATH_CONV "lrrr" o ONCE_REWRITE_CONV o list o SYM o SPECL [`x:num`; `c:num`]) THEN  
   USE_THEN "H5" (REWRITE_TAC o list) THEN 
   EXPAND_TAC "j" THEN 
   EXPAND_TAC "d" THEN 
   SUBGOAL_THEN_MESON[] `c * x * u = u * x * c` (ONCE_REWRITE_TAC o list) THEN 
   SUBGOAL_THEN_MESON[] `!p. neg p * u = u * neg p` (ONCE_REWRITE_TAC o list) THEN 
   ASM_MESON_TAC[];
  (* Step 7 *)
  ASM_REWRITE_TAC[] THEN 
  USE_THEN "ROB" (CONV_TAC o PATH_CONV "lr" o ONCE_REWRITE_CONV o list o SYM o SPECL [`j:num`; `x * neg c:num`]) THEN      
  USE_THEN "H5" (REWRITE_TAC o list) THEN 
  USE_THEN "H3" (REWRITE_TAC o list) THEN 
  USE_THEN "ROB" (CONV_TAC o PATH_CONV "r" o ONCE_REWRITE_CONV o list o SYM o SPECL [`neg c:num`; `j * x:num`]) THEN      
  USE_THEN "H6" (REWRITE_TAC o list) THEN 
  SUBGOAL_THEN_MESON[] `neg c * u = u * neg c` (REWRITE_TAC o list) THEN 
  USE_THEN "H2" (REWRITE_TAC o list) THEN 
  ASM_MESON_TAC[];
]]]]]]]);;
